[1.95.0] Document provenance and its use in const eval#707
[1.95.0] Document provenance and its use in const eval#707kirtchev-adacore wants to merge 3 commits into
Conversation
812a13f to
ecca0f0
Compare
ecca0f0 to
21bb6de
Compare
21bb6de to
e42d104
Compare
The information has been taken from - [core::ptr Provenance](https://doc.rust-lang.org/core/ptr/index.html#provenance) - [reference#2091](rust-lang/reference#2091) - [reference#2139](rust-lang/reference#2138)
e42d104 to
1844443
Compare
|
This PR was rebased onto a different main commit. Here's a range-diff highlighting what actually changed. Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers. |
1844443 to
e23ca4b
Compare
e23ca4b to
a8393ef
Compare
There was a problem hiding this comment.
Hey @kirtchev-adacore, thanks for taking the time to write this up.
I spotted some things we could tune up here and there for precision and to match current understandings for provenance that seem to exist in the Project.
I know the release is tomorrow and we meet Friday, but hopefully this is not too much 😅
| :t:`constant initializer`. | ||
|
|
||
| :dp:`fls_l1FOH8zt0XRZ` | ||
| If the :t:`value` produced by evaluating a :t:`constant initializer` is a :t:`pointer`, then the :t:`pointer` shall be a :t:`well-formed pointer`. |
There was a problem hiding this comment.
This is not intended to be addressed in #707, but it's something I noticed we could do a follow-up on. If this looks reasonable I can go open an issue for it. Lemme know.
The well-formedness rules being added in #707 cover the pointer-fragment restriction from rust-lang/rust#148259, but rustc enforces a second condition on final values that the FLS won't yet capture: a provenance-carrying pointer in the final value must not point to an allocation freed during evaluation.
const P: *const u8 = { let x = 0u8; &raw const x };Current rustc rejects this with "encountered dangling pointer in final value of constant". Note that it seems this predates rust-lang/rust#148259.
Scope note: the condition attaches to pointers in the final value. Allocations created and freed during evaluation are fine as long as no provenance-carrying pointer to them survives into the final value.
Note the existing FLS dangling term can't be reused as-is: it counts null as dangling, while const N: *const u8 = core::ptr::null(); is a legal constant. A liveness-only condition (the provenance's allocated object still exists at the end of evaluation) would need its own wording.
There was a problem hiding this comment.
How about adding "non-dangling" to the definition of "well-formed pointer"?
A :dt:`well-formed pointer` is a non-dangling :t:`pointer` where either no byte
of the :t:`pointer` carries :t:`provenance`, or every byte of the :t:`pointer`
is the corresponding byte of a single :t:`pointer` with :t:`provenance`.There was a problem hiding this comment.
Thanks for going for it, but "non-dangling" specifically would reintroduce the exact bug we just fixed, through the side door. The FLS's dangling is defined as "either null or not all of the bytes at the referred memory location are part of the same allocation", so a non-dangling requirement in well-formed pointer makes these illegal again:
const N: *const u8 = core::ptr::null(); // null => dangling
const D: *const u8 = core::ptr::without_provenance(16); // no allocation => danglingBoth compile today, and both made it through through the definition we just landed via the no-provenance arm.
It looks like the compiler's actual condition is narrower on two axes:
-
It only bites pointers with provenance, so null and
without_provenancepointers are exempt by construction. -
This is a property of the final value, not of pointers generally. Holding a dangling pointer during evaluation seems fine:
const OK: u8 = { let p = { let x = 5u8; &raw const x }; // x is gone; p dangles for the rest of evaluation — fine, // because p never reaches the final value. let _ = p; 0 };
pdangles the momentxdrops, and this compiles.
So folding it into well-formed pointer puts a final-value-only condition into a term that reads like a general pointer property which might be a bit like a trap for whoever reuses the term next.
Maybe we can keep #707 as it now stands and do this as the follow-up: some kind of separate legality rule on the const/static side, something in the direction of "if the value ... contains a pointer with provenance, the allocated object the provenance covers shall not have been deallocated during evaluation."
If that seems okay, I can open the issue with that draft and a link back here.
There was a problem hiding this comment.
How about this gymnastic then:
A :dt:`well-formed pointer` is a :t:`pointer` where either no byte
of the :t:`pointer` carries :t:`provenance`, or every byte of the :t:`pointer`
is the corresponding byte of a single :t:`pointer` with :t:`provenance`.(non-dangling removed)
If the :t:`value` produced by evaluating a :t:`constant initializer` is a :t:`pointer`,
then the :t:`pointer` shall be a non-dangling :t:`well-formed pointer`.(non-dangling added)
1f1b867 to
e1d4a62
Compare
| A :t:`pointer` is a :t:`value` of a :t:`pointer type`. | ||
|
|
||
| :dp:`fls_VWUlxTy0QF9d` | ||
| An :t:`original pointer` is a :t:`pointer` created via allocation. |
There was a problem hiding this comment.
Yep, you're right that the core::ptr quote settles it; I had the model wrong on borrows. If each allocation has a unique Original Pointer and provenance is "implicitly inherited by all pointers transitively derived" from it, then &x and &raw const x are derived.
Two refinements we could consider on the wording, both small:
-
For the original-pointer definition, "a unique pointer for an allocation" leaves the uniqueness ambiguous (unique in what sense?), and the FLS already has the term for the memory side. Here's an attempt to tie both down:
Suggested changeAn :t:`original pointer` is a :t:`pointer` created via allocation. An :t:`original pointer` is the unique :t:`pointer` produced when an :t:`allocated object` is created. ("the unique pointer produced when ... is created" is the
core::ptrsentence restated with the FLS's own term;:dt:variant for the glossary.) -
Your expanded derived list looks correct to me! I poked around for provenance-preserving operations that escape it and came up empty:
with_addr/map_addrare documented as equivalent to wrapping pointer arithmetic, union type punning is a load, argument passing is a copy, reborrows are borrows. Maybe just a little role/phrasing polish?Suggested changeAn :t:`original pointer` is a :t:`pointer` created via allocation. A :t:`derived pointer` is a :t:`pointer` obtained by :t:`borrowing`, copying a :t:`pointer`, loading a stored :t:`pointer`, performing :t:`pointer` arithmetic, or :t:`casting` a :t:`pointer`. (
borrowingandcastinglook to be existing glossary terms, so maybe we link and use them?)
One optional consequence of your model, maybe to consider: with borrows demoted to derived, the Original Pointer's provenance must cover everything any derived pointer can ever access — i.e. the entire allocated object. So fls_1NJhTBN1D2qv could now drop "all or part" and say the original pointer carries provenance over the allocated object it was created from, with all narrowing living in derivation. "All or part" stays true either way, so maybe not a big deal.
| :t:`constant initializer`. | ||
|
|
||
| :dp:`fls_l1FOH8zt0XRZ` | ||
| If the :t:`value` produced by evaluating a :t:`constant initializer` is a :t:`pointer`, then the :t:`pointer` shall be a :t:`well-formed pointer`. |
There was a problem hiding this comment.
Thanks for going for it, but "non-dangling" specifically would reintroduce the exact bug we just fixed, through the side door. The FLS's dangling is defined as "either null or not all of the bytes at the referred memory location are part of the same allocation", so a non-dangling requirement in well-formed pointer makes these illegal again:
const N: *const u8 = core::ptr::null(); // null => dangling
const D: *const u8 = core::ptr::without_provenance(16); // no allocation => danglingBoth compile today, and both made it through through the definition we just landed via the no-provenance arm.
It looks like the compiler's actual condition is narrower on two axes:
-
It only bites pointers with provenance, so null and
without_provenancepointers are exempt by construction. -
This is a property of the final value, not of pointers generally. Holding a dangling pointer during evaluation seems fine:
const OK: u8 = { let p = { let x = 5u8; &raw const x }; // x is gone; p dangles for the rest of evaluation — fine, // because p never reaches the final value. let _ = p; 0 };
pdangles the momentxdrops, and this compiles.
So folding it into well-formed pointer puts a final-value-only condition into a term that reads like a general pointer property which might be a bit like a trap for whoever reuses the term next.
Maybe we can keep #707 as it now stands and do this as the follow-up: some kind of separate legality rule on the const/static side, something in the direction of "if the value ... contains a pointer with provenance, the allocated object the provenance covers shall not have been deallocated during evaluation."
If that seems okay, I can open the issue with that draft and a link back here.
e1d4a62 to
979328b
Compare
The information has been taken from